(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun o () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g (Int Int Int) Int)
(declare-fun h () Int)
(declare-fun i (Int) Int)
(declare-fun j (Int) Int)
(declare-fun k (Int) Int)
(declare-fun l (Int) Int)
(declare-fun m (Int) Bool)
(declare-fun n (Int) Bool)
(assert (let ((p (n (i (i 0))))) (let ((aa p)(ab (m 0))) (let ((af (n 0))(ag (or (m f) (n e)))) (let ((al (distinct 0 d))(q (not (n (i 0))))(an h)(aq (n 0))) (let ((bs (ite ag (+ 1 c) c))) (let ((av (ite af 0 bs))) (let ((au (ite (not (distinct c av)) (+ 1 c) c))) (let ((az b)) (let ((be (ite ab (- 0 8 av) av))) (let ((bg (ite (and p (distinct au be)) (- au) au))) (let ((bk (distinct b (k 0)))) (let ((cb (or (and (or (m (i 0)) p) (or bk (= bg c)))))) (let ((ce (and ab (distinct (l 0) d)))) (let ((cq (g (ite (= an bs) 0 (ite (and ag (distinct c an)) 0 o)) 0 a))) (not (and al (= (ite ce av (ite af bs c)) au) (= (ite (not (distinct bg (ite aa (* 20 be) be))) (ite cb (g 0 (ite (or ab (and af bk)) a (ite (and ab ag) (ite ag (g 0 a a) a) (ite q cq 0))) (ite (and ab (not (= b (j 0)))) a 0)) (ite q cq (ite (or aq (and ag (= bg c))) (g 0 a a) a))) 0) 0))))))))))))))))))
(check-sat)
